w:World. FairFifo  (e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id)) 

latex

Definitions	t  T, P  Q, x:A. B(x), loc(e), <a, b>, Id, s = t, E, w-pred(w;e), x.A(x), pred(e), World, FairFifo, first(e), b, A, loc(e)
Lemmas	not wf, assert wf, first wf, fair-fifo wf, world wf, w-loc-lemma, pred wf, w-pred wf, w-E wf, w-loc-w-pred